1. Technical Field
The present invention relates to computer program checking and more particularly to a system and method for analyzing a concurrent program with predictive analysis which employs a Universal Causality Graph (UCG).
2. Description of the Related Art
Predictive analysis aims at detecting concurrency errors such as atomicity violations by analyzing a concrete execution trace (which itself may be non-erroneous). In its most general form, predictive analysis has three main steps: 1) Run a test of the concurrent program to obtain an execution trace. 2) Run a sound but over-approximate algorithm, typically involving statically analyzing the given trace, to detect all potential violations, e.g., data races, deadlocks, atomicity violations, etc. If no violation is found, return. 3) Build the precise predictive model, and for each potential violation, check whether it is feasible. If it is feasible, create a concrete and replayable witness trace. This check is typically formulated as a satisfiability problem, by constructing a formula which is satisfiable if there exists a feasible trace that exposes a potential error.
In this framework, step 2, i.e., a static enumeration of the set of interleavings that may potentially lead to a concurrency violation, occupies a key role in determining scalability as well as precision of the overall procedure.
Existing predictive analysis algorithms can be classified into the following categories: 1) Methods that do not miss real errors but may report bogus errors. These methods are based on over approximated modeling of the execution trace. Representatives are based on causal atomicity, and based on type-for-atomicity. 2) Methods that do not report bogus errors but may miss some real errors. These methods are based on under-approximated modeling. Representatives are based on happens-before causality relations. 3) Methods that are both sound and complete but not scalable as they explore too many interleavings.